/-
Copyright (c) 2025 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
module

public import Mathlib.AlgebraicTopology.SimplicialSet.Basic
public import Mathlib.CategoryTheory.Subpresheaf.OfSection

/-!
# Subcomplexes of a simplicial set

Given a simplicial set `X`, this file defines the type `X.Subcomplex`
of subcomplexes of `X` as an abbreviation for `Subpresheaf X`.
It also introduces a coercion from `X.Subcomplex` to `SSet`.

## Implementation note

`SSet.{u}` is defined as `Cᵒᵖ ⥤ Type u`, but it is not an abbreviation.
This is the reason why `Subpresheaf.ι` is redefined here as `Subcomplex.ι`
so that this morphism appears as a morphism in `SSet` instead of a morphism
in the category of presheaves.

-/

@[expose] public section

universe u

open CategoryTheory Simplicial Limits

namespace SSet

-- Note: this could be obtained as `inferInstanceAs (Balanced (_ ⥤ _))`
-- by importing `Mathlib.CategoryTheory.Adhesive`, but we give a
-- different proof so as to reduce imports
instance : Balanced SSet.{u} where
  isIso_of_mono_of_epi f _ _ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro
    rw [isIso_iff_bijective]
    constructor
    · rw [← mono_iff_injective]
      infer_instance
    · rw [← epi_iff_surjective]
      infer_instance

variable (X Y : SSet.{u})

/-- The complete lattice of subcomplexes of a simplicial set. -/
abbrev Subcomplex := Subpresheaf X

variable {X Y}

namespace Subcomplex

/-- The underlying simplicial set of a subcomplex. -/
abbrev toSSet (A : X.Subcomplex) : SSet.{u} := A.toPresheaf

instance : CoeOut X.Subcomplex SSet.{u} where
  coe := fun S ↦ S.toSSet

instance {X : SSet.{u}} (n : SimplexCategoryᵒᵖ) (A : X.Subcomplex)
    [DecidableEq (X.obj n)] :
    DecidableEq ((A : SSet).obj n) :=
  inferInstanceAs (DecidableEq (A.obj n))

/-- If `A : Subcomplex X`, this is the inclusion `A ⟶ X` in the category `SSet`. -/
abbrev ι (A : Subcomplex X) : Quiver.Hom (V := SSet) A X := Subpresheaf.ι A

instance (A : X.Subcomplex) : Mono A.ι :=
  inferInstanceAs (Mono (Subpresheaf.ι A))

section

variable {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂)

/-- Given an inequality `S₁ ≤ S₂` between subcomplexes of a simplicial set,
this is the induced morphism in the category `SSet`. -/
abbrev homOfLE : (S₁ : SSet.{u}) ⟶ (S₂ : SSet.{u}) := Subpresheaf.homOfLe h

@[reassoc]
lemma homOfLE_comp {S₃ : X.Subcomplex} (h' : S₂ ≤ S₃) :
    homOfLE h ≫ homOfLE h' = homOfLE (h.trans h') := rfl

variable (S₁) in
@[simp]
lemma homOfLE_refl : homOfLE (by rfl : S₁ ≤ S₁) = 𝟙 _ := rfl

@[simp]
lemma homOfLE_app_val (Δ : SimplexCategoryᵒᵖ) (x : S₁.obj Δ) :
    ((homOfLE h).app Δ x).val = x.val := rfl

@[reassoc (attr := simp)]
lemma homOfLE_ι : homOfLE h ≫ S₂.ι = S₁.ι := rfl

instance mono_homOfLE : Mono (homOfLE h) := mono_of_mono_fac (homOfLE_ι h)

/-- This is the isomorphism of simplicial sets corresponding to
an equality of subcomplexes. -/
@[simps]
protected def eqToIso (h : S₁ = S₂) : (S₁ : SSet.{u}) ≅ S₂ where
  hom := homOfLE h.le
  inv := homOfLE h.symm.le

end

/-- The functor which sends `A : X.Subcomplex` to `A.toSSet`. -/
@[simps]
def toSSetFunctor : X.Subcomplex ⥤ SSet.{u} where
  obj A := A
  map h := homOfLE (leOfHom h)

section

variable (X)

/-- If `X : SSet`, this is the isomorphism of simplicial sets
from `⊤ : X.Subcomplex` to `X`. -/
@[simps! inv_app_coe]
def topIso : ((⊤ : X.Subcomplex) : SSet) ≅ X :=
  NatIso.ofComponents (fun n ↦ (Equiv.Set.univ (X.obj n)).toIso)

@[simp]
lemma topIso_hom : (topIso X).hom = Subcomplex.ι _ := rfl

@[reassoc (attr := simp)]
lemma topIso_inv_ι : (topIso X).inv ≫ Subpresheaf.ι _ = 𝟙 _ := rfl

end

instance : Subsingleton (((⊥ : X.Subcomplex) : SSet.{u}) ⟶ Y) where
  allEq _ _ := by ext _ ⟨_, h⟩; simp at h

instance : Unique (((⊥ : X.Subcomplex) : SSet.{u}) ⟶ Y) where
  default :=
    { app := by rintro _ ⟨_, h⟩; simp at h
      naturality _ _ _ := by ext ⟨_, h⟩; simp at h }
  uniq := by subsingleton

/-- If `X` is a simplicial set, then the empty subcomplex of `X` is an initial
object in `SSet`. -/
def isInitialBot : IsInitial ((⊥ : X.Subcomplex) : SSet.{u}) :=
  IsInitial.ofUnique _

/-- The subcomplex of a simplicial set that is generated by a simplex. -/
abbrev ofSimplex {n : ℕ} (x : X _⦋n⦌) : X.Subcomplex := Subpresheaf.ofSection x

lemma mem_ofSimplex_obj {n : ℕ} (x : X _⦋n⦌) :
    x ∈ (ofSimplex x).obj _ :=
  Subpresheaf.mem_ofSection_obj x

lemma ofSimplex_le_iff {n : ℕ} (x : X _⦋n⦌) (A : X.Subcomplex) :
    ofSimplex x ≤ A ↔ x ∈ A.obj _ :=
  Subpresheaf.ofSection_le_iff _ _

lemma mem_ofSimplex_obj_iff {n : ℕ} (x : X _⦋n⦌) {m : SimplexCategoryᵒᵖ} (y : X.obj m) :
    y ∈ (ofSimplex x).obj m ↔ ∃ (f : m.unop ⟶ ⦋n⦌), X.map f.op x = y := by
  dsimp [ofSimplex, Subpresheaf.ofSection]
  aesop

section

variable (f : X ⟶ Y)

/-- The range of a morphism of simplicial sets, as a subcomplex. -/
abbrev range : Y.Subcomplex := Subpresheaf.range f

/-- The morphism `X ⟶ Subcomplex.range f` induced by `f : X ⟶ Y`. -/
abbrev toRange : X ⟶ Subcomplex.range f := Subpresheaf.toRange f

@[reassoc (attr := simp)]
lemma toRange_ι : toRange f ≫ (Subcomplex.range f).ι = f := rfl

@[simp]
lemma toRange_app_val {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ) :
    ((toRange f).app Δ x).val = f.app Δ x := rfl

instance : Epi (toRange f) :=
  inferInstanceAs (Epi (Subpresheaf.toRange f))

instance [Mono f] : Mono (toRange f) :=
  mono_of_mono_fac (toRange_ι f)

instance [Mono f] : IsIso (toRange f) :=
  isIso_of_mono_of_epi _

lemma range_eq_top_iff : Subcomplex.range f = ⊤ ↔ Epi f := by
  rw [NatTrans.epi_iff_epi_app, Subpresheaf.ext_iff, funext_iff]
  simp only [epi_iff_surjective, Subpresheaf.range_obj, Subpresheaf.top_obj,
    Set.top_eq_univ, Set.range_eq_univ]

lemma range_eq_top [Epi f] : Subcomplex.range f = ⊤ := by
  rwa [range_eq_top_iff]

end

section

variable (f : X ⟶ Y) {B : Y.Subcomplex} (hf : range f ≤ B)

/-- Given a morphism of simplicial sets `f : X ⟶ Y` whose
range is `≤ B` for some `B : Y.Subcomplex`, this is the
induced morphism `X ⟶ B`. -/
def lift : X ⟶ B := Subpresheaf.lift f hf

@[reassoc (attr := simp)]
lemma lift_ι : lift f hf ≫ B.ι = f := rfl

@[simp]
lemma lift_app_coe {n : SimplexCategoryᵒᵖ} (x : X.obj n) :
    ((lift f hf).app _ x).1 = f.app _ x := rfl

end

section

/-- The preimage of a subcomplex by a morphism of simplicial sets. -/
@[simps]
def preimage (A : X.Subcomplex) (p : Y ⟶ X) : Y.Subcomplex where
  obj n := p.app n ⁻¹' (A.obj n)
  map f := (Set.preimage_mono (A.map f)).trans (by
    simp only [Set.preimage_preimage, FunctorToTypes.naturality _ _ p f]
    rfl)

@[simp]
lemma preimage_max (A B : X.Subcomplex) (p : Y ⟶ X) :
    (A ⊔ B).preimage p = A.preimage p ⊔ B.preimage p := rfl

@[simp]
lemma preimage_min (A B : X.Subcomplex) (p : Y ⟶ X) :
    (A ⊓ B).preimage p = A.preimage p ⊓ B.preimage p := rfl

@[simp]
lemma preimage_iSup {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) :
    (⨆ i, A i).preimage p = ⨆ i, (A i).preimage p := by aesop

@[simp]
lemma preimage_iInf {ι : Type*} (A : ι → X.Subcomplex) (p : Y ⟶ X) :
    (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p := by aesop

end

section

variable (A : X.Subcomplex) (f : X ⟶ Y)

/-- The image of a subcomplex by a morphism of simplicial sets. -/
@[simps!]
def image : Y.Subcomplex := Subpresheaf.image A f

lemma image_le_iff (Z : Y.Subcomplex) :
    A.image f ≤ Z ↔ A ≤ Z.preimage f := by
  simp [Subpresheaf.le_def]

lemma image_top : (⊤ : X.Subcomplex).image f = range f := by aesop

@[simp]
lemma image_id : A.image (𝟙 _) = A := by aesop

lemma image_comp {Z : SSet.{u}} (g : Y ⟶ Z) :
    A.image (f ≫ g) = (A.image f).image g := by aesop

lemma range_comp {Z : SSet.{u}} (g : Y ⟶ Z) :
    Subcomplex.range (f ≫ g) = (Subcomplex.range f).image g := by aesop

lemma image_eq_range : A.image f = range (A.ι ≫ f) := by aesop

lemma image_iSup {ι : Type*} (S : ι → X.Subcomplex) (f : X ⟶ Y) :
    image (⨆ i, S i) f = ⨆ i, (S i).image f := by
  aesop

@[simp]
lemma preimage_range : (range f).preimage f = ⊤ :=
  le_antisymm (by simp) (by rw [← image_le_iff, image_top])

@[simp]
lemma image_le_range : A.image f ≤ range f := by
  simp [image_le_iff, preimage_range, le_top]

@[simp]
lemma image_ofSimplex {n : ℕ} (x : X _⦋n⦌) (f : X ⟶ Y) :
    (ofSimplex x).image f = ofSimplex (f.app _ x) := by
  apply le_antisymm
  · rw [image_le_iff, ofSimplex_le_iff, preimage_obj, Set.mem_preimage]
    apply mem_ofSimplex_obj
  · rw [ofSimplex_le_iff]
    exact ⟨x, mem_ofSimplex_obj _, rfl⟩

/-- Given a morphism of simplicial sets `f : X ⟶ Y` and a subcomplex `A` of `X`,
this is the induced morphism from `A` to `A.image f`. -/
@[simps!]
def toImage : (A : SSet) ⟶ (A.image f : SSet) :=
  (A.image f).lift (A.ι ≫ f) (by rw [image_eq_range])

@[reassoc (attr := simp)]
lemma toImage_ι : A.toImage f ≫ (A.image f).ι = A.ι ≫ f := rfl

instance : Epi (A.toImage f) := by
  rw [← range_eq_top_iff]
  apply le_antisymm (by simp)
  rintro m ⟨_, ⟨y, hy, rfl⟩⟩ _
  exact ⟨⟨y, hy⟩, rfl⟩

lemma image_monotone : Monotone (fun (S : X.Subcomplex) ↦ S.image f) := by
  intro S T h
  rw [image_le_iff]
  exact h.trans (by rw [← image_le_iff])

end

lemma preimage_eq_top_iff (B : X.Subcomplex) (f : Y ⟶ X) :
    B.preimage f = ⊤ ↔ range f ≤ B := by
  rw [← image_top, image_le_iff, top_le_iff]

@[simp]
lemma image_preimage_le (B : X.Subcomplex) (f : Y ⟶ X) :
    (B.preimage f).image f ≤ B := by
  rw [image_le_iff]

/-- Given a morphism of simplicial sets `p : Y ⟶ X` and
`A : X.Subcomplex`, this is the induced morphism
`(A.preimage p : SSet) ⟶ (A : SSet)`. -/
@[simps!]
def fromPreimage (A : X.Subcomplex) (p : Y ⟶ X) :
    (A.preimage p : SSet) ⟶ (A : SSet) :=
  lift (Subcomplex.ι _ ≫ p) (by simp [range_comp])

@[reassoc (attr := simp)]
lemma fromPreimage_ι (A : X.Subcomplex) (p : Y ⟶ X) :
    A.fromPreimage p ≫ A.ι = (A.preimage p).ι ≫ p := rfl

end Subcomplex

end SSet
